(declare-fun _substvar_150_ () Real)
(declare-const r1 Real)
(declare-const r10 Real)
(declare-const r18 Real)
(declare-const r20 Real)
(declare-const v22 Bool)
(declare-const r24 Real)
(declare-const v34 Bool)
(assert (< 0.6463 r24 0.0 _substvar_150_ (/ 57359.0 0.0)))
(assert (or (< 0.0 0.5277230151 r20 0.0 (* r18 (/ 325285732.0 r10) (/ 0.0 0.0) r20)) (< 0.0 3.0 (/ (+ 0.0 (/ 0.5277230151 0.0) (/ 325285732.0 r10)) r1) r10)))
(check-sat)
